Termination Proof Script

• Consider the SCC {21}. There are no usable rules. By taking the AF π with π(APP) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 21 is strictly decreasing.


• Consider the SCC {27}. There are no usable rules. By taking the AF π with π(PLUS) = 1 together with the lexicographic path order with empty precedence, rule 27 is strictly decreasing.


• Consider the SCC {16,19}. The usable rules are {5,6}. By taking the AF π with π(MINUS) = π(s) = 1, π(plus) = 2 and π(minus) = [1] together with the lexicographic path order with empty precedence, the rules in {5,6,16} are weakly decreasing and rule 19 is strictly decreasing. There is one new SCC.
  • Consider the SCC {16}. There are no usable rules. By taking the AF π with π(MINUS) = 1 together with the lexicographic path order with empty precedence, rule 16 is strictly decreasing.


• Consider the SCC {17}. The usable rules are {1,2,5-7}. By taking the AF π with π(minus) = π(QUOT) = 1 together with the lexicographic path order with precedence plus ≻ s, the rules in {1,7} are weakly decreasing and the rules in {2,5,6,17} are strictly decreasing.


• Consider the SCC {22}. The usable rules are {5,6}. By taking the AF π with π(s) = π(SUM) = 1, π(plus) = 2 and π(cons) = [2] together with the lexicographic path order with empty precedence, the rules in {5,6} are weakly decreasing and rule 22 is strictly decreasing.


• Consider the SCC {24}. The usable rules are {5,6,8-13}. The constraints could not be solved.